Nuprl Definition : imon
13,42
postcript
pdf
IMonoid == {
g
:GrpSig| IsMonoid(|
g
|;*;e)}
latex
clarification:
IMonoid{i} == {
g
:GrpSig{i}| IsMonoid(|
g
|;*
g
;e
g
)}
latex
Up
groups
1
Wellformedness Lemmas
imon
wf
Definitions
GrpSig
,
IsMonoid(
T
;
op
;
id
)
,
|
g
|
,
*
,
e
origin